@i Precondition for a(Outcome(p)) 
@i P discrete state(ds)
== (x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
== c (alle-at(es;
== c (alle-at(i;
== c (alle-at(e.((es-kind(es; e) = locl(a))
== c (alle-at( (subtype_rel(es-valtype(es; e); p-outcome(p)) c ((P(es-state-when(es; e)))))))
== c  (@i discrete ds
== c   (alle-at(es;
== c   (alle-at(i;
== c   (alle-at(e.existse-ge(es;
== c   (alle-at(e.existse-ge(e;
== c   (alle-at(e.existse-ge(e'.((es-kind(es; e') = locl(a))
== c   (alle-at(e.existse-ge( (((P(es-state-after(es; e'))))))))
== c    (((P(es-init-state(es; i))))  (e:es-E(es). (loc(e) = i)))))) 

latex

---

clarification:

discrete-pre-p(es;i;ds;a;p;P)
== (x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
== c (alle-at(es;
== c (alle-at(i;
== c (alle-at(e.((es-kind(es; e) = locl(a)  Knd)
== c (alle-at( (subtype_rel(es-valtype(es; e); p-outcome(p)) c ((P(es-state-when(es; e)))))))
== c  (es-dds(es;i;ds)
== c   (alle-at(es;
== c   (alle-at(i;
== c   (alle-at(e.existse-ge(es;
== c   (alle-at(e.existse-ge(e;
== c   (alle-at(e.existse-ge(e'.((es-kind(es; e') = locl(a)  Knd)
== c   (alle-at(e.existse-ge( (((P(es-state-after(es; e'))))))))
== c    (((P(es-init-state(es; i))))  (e:es-E(es). (es-loc(es; e) = i  Id)))))) 

latex

Definitions	x:A. B(x), es-vartype(es; i; x), fpf-cap(f; eq; x; z), id-deq, top, A c B, es-valtype(es; e), p-outcome(p), es-state-when(es; e), @i discrete ds, P  Q, alle-at(es; i; e.P(e)), existse-ge(es; e; e'.P(e')), P  Q, Knd, es-kind(es; e), locl(a), A, es-state-after(es; e), P  Q, b, f(a), es-init-state(es; i), x:A. B(x), es-E(es), s = t, Id, loc(e)
FDL editor aliases	discrete-pre-p